Proving Termination by Dependency Pairs and Inductive Theorem Proving
Identifieur interne : 002647 ( Main/Exploration ); précédent : 002646; suivant : 002648Proving Termination by Dependency Pairs and Inductive Theorem Proving
Auteurs : Carsten Fuhs [Allemagne] ; Jürgen Giesl [Allemagne] ; Michael Parting [Allemagne] ; Peter Schneider-Kamp [Danemark] ; Stephan Swiderski [Allemagne]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 2011-08-01.
English descriptors
- KwdEn :
Abstract
Abstract: Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for termination of TRSs with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.
Url:
DOI: 10.1007/s10817-010-9215-9
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002386
- to stream Istex, to step Curation: 002355
- to stream Istex, to step Checkpoint: 000547
- to stream Main, to step Merge: 002689
- to stream Main, to step Curation: 002647
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Proving Termination by Dependency Pairs and Inductive Theorem Proving</title><author><name sortKey="Fuhs, Carsten" sort="Fuhs, Carsten" uniqKey="Fuhs C" first="Carsten" last="Fuhs">Carsten Fuhs</name></author><author><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name></author><author><name sortKey="Parting, Michael" sort="Parting, Michael" uniqKey="Parting M" first="Michael" last="Parting">Michael Parting</name></author><author><name sortKey="Schneider Kamp, Peter" sort="Schneider Kamp, Peter" uniqKey="Schneider Kamp P" first="Peter" last="Schneider-Kamp">Peter Schneider-Kamp</name></author><author><name sortKey="Swiderski, Stephan" sort="Swiderski, Stephan" uniqKey="Swiderski S" first="Stephan" last="Swiderski">Stephan Swiderski</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:99B5DE0CD006C840C4A13B7F45A198B745D6DADF</idno><date when="2011" year="2011">2011</date><idno type="doi">10.1007/s10817-010-9215-9</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-6STSK0F7-5/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002386</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002386</idno><idno type="wicri:Area/Istex/Curation">002355</idno><idno type="wicri:Area/Istex/Checkpoint">000547</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000547</idno><idno type="wicri:doubleKey">0168-7433:2011:Fuhs C:proving:termination:by</idno><idno type="wicri:Area/Main/Merge">002689</idno><idno type="wicri:Area/Main/Curation">002647</idno><idno type="wicri:Area/Main/Exploration">002647</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Proving Termination by Dependency Pairs and Inductive Theorem Proving</title><author><name sortKey="Fuhs, Carsten" sort="Fuhs, Carsten" uniqKey="Fuhs C" first="Carsten" last="Fuhs">Carsten Fuhs</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Aachen</wicri:regionArea><placeName><region type="land" nuts="1">Rhénanie-du-Nord-Westphalie</region><region type="district" nuts="2">District de Cologne</region><settlement type="city">Aix-la-Chapelle</settlement></placeName></affiliation></author><author><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Aachen</wicri:regionArea><placeName><region type="land" nuts="1">Rhénanie-du-Nord-Westphalie</region><region type="district" nuts="2">District de Cologne</region><settlement type="city">Aix-la-Chapelle</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Parting, Michael" sort="Parting, Michael" uniqKey="Parting M" first="Michael" last="Parting">Michael Parting</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Aachen</wicri:regionArea><placeName><region type="land" nuts="1">Rhénanie-du-Nord-Westphalie</region><region type="district" nuts="2">District de Cologne</region><settlement type="city">Aix-la-Chapelle</settlement></placeName></affiliation></author><author><name sortKey="Schneider Kamp, Peter" sort="Schneider Kamp, Peter" uniqKey="Schneider Kamp P" first="Peter" last="Schneider-Kamp">Peter Schneider-Kamp</name><affiliation wicri:level="1"><country xml:lang="fr">Danemark</country><wicri:regionArea>Department of Mathematics & Computer Science, University of Southern Denmark, Odense</wicri:regionArea><wicri:noRegion>Odense</wicri:noRegion></affiliation></author><author><name sortKey="Swiderski, Stephan" sort="Swiderski, Stephan" uniqKey="Swiderski S" first="Stephan" last="Swiderski">Stephan Swiderski</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Aachen</wicri:regionArea><placeName><region type="land" nuts="1">Rhénanie-du-Nord-Westphalie</region><region type="district" nuts="2">District de Cologne</region><settlement type="city">Aix-la-Chapelle</settlement></placeName></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">J Autom Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Springer Netherlands</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2011-08-01">2011-08-01</date><biblScope unit="volume">47</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="133">133</biblScope><biblScope unit="page" to="160">160</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Dependency pairs</term><term>Induction</term><term>Term rewriting</term><term>Termination</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for termination of TRSs with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>Danemark</li></country><region><li>District de Cologne</li><li>Rhénanie-du-Nord-Westphalie</li></region><settlement><li>Aix-la-Chapelle</li></settlement></list><tree><country name="Allemagne"><region name="Rhénanie-du-Nord-Westphalie"><name sortKey="Fuhs, Carsten" sort="Fuhs, Carsten" uniqKey="Fuhs C" first="Carsten" last="Fuhs">Carsten Fuhs</name></region><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name><name sortKey="Parting, Michael" sort="Parting, Michael" uniqKey="Parting M" first="Michael" last="Parting">Michael Parting</name><name sortKey="Swiderski, Stephan" sort="Swiderski, Stephan" uniqKey="Swiderski S" first="Stephan" last="Swiderski">Stephan Swiderski</name></country><country name="Danemark"><noRegion><name sortKey="Schneider Kamp, Peter" sort="Schneider Kamp, Peter" uniqKey="Schneider Kamp P" first="Peter" last="Schneider-Kamp">Peter Schneider-Kamp</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002647 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 002647 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:99B5DE0CD006C840C4A13B7F45A198B745D6DADF
|texte= Proving Termination by Dependency Pairs and Inductive Theorem Proving
}}
| This area was generated with Dilib version V0.6.33. |  |